Temporal logics are various forms of formal logic desigend to deal with things that change over time. Many deal with sequence of state of the word rather than real time andbuild on basic propositional ligic or predicate logic by adding new temporal operators. These may include always P (usually written as a square), meaning at all times from now on P will be true, and eventually P (usually written as a diamond), meaning that now or at some future time P will be true. Temporal logics are usually divided into linear time temporal logics that model times asa. simpe sequence of tiem steps, and branching time temporal logics, which consider multiple possible futures.
